1 /-
2 Copyright (c) 2018 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Chris Hughes
5 -/
6 import group_theory.group_action group_theory.quotient_group
src └───────────────────────┘ └─────────────────────────┘
7 import group_theory.order_of_element data.zmod.basic
src └───────────────────────────┘ └─────────────┘
8
9 open equiv fintype finset mul_action function
10 open equiv.perm is_subgroup list quotient_group
11 universes u v w
12 variables {G : Type u} {α : Type v} {β : Type w} [group G]
id ┴ ┴└───┘
src └───┘
typ ┴ ┴└───┘
13
14 local attribute [instance, priority 10] subtype.fintype set_fintype classical.prop_decidable
id └─────────────┘ └─────────┘ └──────────────────────┘
src └─────────────┘ └─────────┘ └──────────────────────┘
typ └─────────────┘ └─────────┘ └──────────────────────┘
15
16 namespace mul_action
17 variables [mul_action G α]
id └────────┘
src └────────┘
typ └────────┘
doc └────────┘
18
19 lemma mem_fixed_points_iff_card_orbit_eq_one {a : α}
id ┴
typ ┴
20 [fintype (orbit G a)] : a ∈ fixed_points G α ↔ card (orbit G a) = 1 :=
id └─────┘ └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
src └─────┘ └───┘ ┴ └──────────┘ ┴ └──┘ └───┘ ┴
typ └─────┘ └───┘ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
doc └─────┘ └──┘
21 begin
st └─────
22 rw [fintype.card_eq_one_iff, mem_fixed_points],
id └─────────────────────┘ └──────────────┘
src └──┘└─────────────────────┘└┘└──────────────┘┴
typ └──┘└─────────────────────┘└┘└──────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────────┘└────────────────┘└──
23 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
24 { exact λ h, ⟨⟨a, mem_orbit_self _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ },
id ┴ └────────────┘ └────────┘ ┴ ┴
src └────┘ └──┘ └┘└────────────┘└───┘ └┘ └┘ └┘ └──┘└────────┘┴ ┴ ┴└────┘ ┴ └┘ ┴└┘
typ └────┘ └──┘ ┴└┘└────────────┘└───┘ └┘ └┘ └┘ └──┘└────────┘┴ ┴ ┴└────┘┴┴┴└┘└─────┘┴└┘
doc └────┘ └──┘ └┘ └───┘ └┘ └┘ └┘ └──┘ ┴ ┴ ┴└────┘ ┴ └┘ ┴└┘
txt └────┘ └──┘ └┘ └───┘ └┘ └┘ └┘ └──┘ ┴ ┴ ┴└────┘ ┴ └┘ ┴└┘
par └────┘ └──┘ └┘ └───┘ └┘ └┘ └┘ └──┘ ┴ ┴ ┴└────┘ ┴ └┘ ┴└┘
pid ┴ └──┘ └┘ └───┘ └┘ └┘ └┘ └──┘ ┴ ┴ └─────┘ ┴ └┘ └┘┴
st ───┘└────────────────────────────────────────────────────────────────┘└──────────────────┘└┘└┘└
25 { assume h x,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ─────────────┘└─
26 rcases h with ⟨⟨z, hz⟩, hz₁⟩,
id ┴
src └─────┘ └──────────────────┘
typ └─────┘┴└──────────────────┘
doc └─────┘ └──────────────────┘
txt └─────┘ └──────────────────┘
par └─────┘ └──────────────────┘
pid ┴ └──────────────────┘
st ───────────────────────────────┘└─
27 exact calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
id ┴ ┴ ┴ └───────┘
src └────┘ ┴ ┴┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘└───────┘└──────
typ └────┘ ┴ ┴┴┴ ┴ ┴┴└─┘ ┴ ┴ ┴┴ ┴ └┘└───────┘└──────
doc └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──────
txt └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──────
par └────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──────
pid ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──────
st ───────────────────────────────────────────────────────────────────────
28 ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm }
id └────────────┘ └─┘ ┴ └────────────┘
src ─────────┘ ┴ └─┘ └────────────┘┴ ┴ └┘└────────────┘└─────────┘
typ ─────────┘ ┴ └─┘ └────────────┘┴ └─┘┴ ┴└┘└────────────┘└─────────┘
doc ─────────┘ ┴ └─┘ ┴ ┴ └┘ └─────────┘
txt ─────────┘ ┴ └─┘ ┴ ┴ └┘ └─────────┘
par ─────────┘ ┴ └─┘ ┴ ┴ └┘ └─────────┘
pid ─────────┘ ┴ └─┘ ┴ ┴ └┘ └───────┘└┘
st ─────────────────────────────────────────────────────────────────┘└─
29 end
st ──┘
30
31 lemma card_modeq_card_fixed_points [fintype α] [fintype G] [fintype (fixed_points G α)]
id └─────┘ ┴ └─────┘ ┴ └─────┘ └──────────┘ ┴ ┴
src └─────┘ └─────┘ └─────┘ └──────────┘
typ └─────┘ ┴ └─────┘ ┴ └─────┘ └──────────┘ ┴ ┴
doc └─────┘ └─────┘ └─────┘
32 {p n : ℕ} (hp : nat.prime p) (h : card G = p ^ n) : card α ≡ card (fixed_points G α) [MOD p] :=
id ┴ └───────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └──────────┘ ┴ ┴ └──┘ ┴┴
src ┴ └───────┘ └──┘ ┴ ┴ └──┘ ┴ └──┘ └──────────┘ └──┘ ┴
typ ┴ └───────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └──────────┘ ┴ ┴ └──┘ ┴┴
doc └───────┘ └──┘ └──┘ ┴ └──┘ └──┘ ┴
33 calc card α = card (Σ y : quotient (orbit_rel G α), {x // quotient.mk' x = y}) :
id └──┘ ┴ └──┘ ┴ └──────┘ └───────┘ ┴ ┴ ┴ ┴┴ └──────────┘ ┴ ┴ ┴
src └──┘ └──┘ ┴ └──────┘ └───────┘ ┴ ┴ └──────────┘ ┴
typ └──┘ ┴ └──┘ ┴ └──────┘ └───────┘ ┴ ┴ ┴ ┴┴ └──────────┘ ┴ ┴ ┴
doc └──┘ └──┘
34 card_congr (sigma_preimage_equiv (@quotient.mk' _ (orbit_rel G α))).symm
id └────────┘ └──────────────────┘ └──────────┘ └───────┘ ┴ ┴ └──┘
src └────────┘ └──────────────────┘ └──────────┘ └───────┘ └──┘
typ └────────┘ └──────────────────┘ └──────────┘ └───────┘ ┴ ┴ └──┘
35 ... = univ.sum (λ a : quotient (orbit_rel G α), card {x // quotient.mk' x = a}) : card_sigma _
id └──┘└──┘ └──────┘ └───────┘ ┴ ┴ └──┘ ┴┴ └──────────┘ ┴ ┴ ┴ └────────┘
src └──┘└──┘ └──────┘ └───────┘ └──┘ ┴ └──────────┘ ┴ └────────┘
typ └──┘└──┘ └──────┘ └───────┘ ┴ ┴ └──┘ ┴┴ └──────────┘ ┴ ┴ ┴ └────────┘
doc └──┘ └──┘
36 ... ≡ (@univ (fixed_points G α) _).sum (λ _, 1) [MOD p] :
id └──┘ └──────────┘ ┴ ┴ └─┘ ┴
src └──┘ └──────────┘ └─┘
typ └──┘ └──────────┘ ┴ ┴ └─┘ ┴
doc └──┘
37 begin
st └─────
38 rw [← zmodp.eq_iff_modeq_nat hp, sum_nat_cast, sum_nat_cast],
id └────────────────────┘ └┘ └──────────┘ └──────────┘
src └────┘└────────────────────┘┴ └┘└──────────┘└┘└──────────┘┴
typ └────┘└────────────────────┘┴└┘└┘└──────────┘└┘└──────────┘┴
doc └────┘ ┴ └┘ └┘ ┴
txt └────┘ ┴ └┘ └┘ ┴
par └────┘ ┴ └┘ └┘ ┴
pid └──┘ ┴ └┘ └┘ ┴
st ────────────────────────────────┘└────────────┘└────────────┘└──
39 refine eq.symm (sum_bij_ne_zero (λ a _ _, quotient.mk' a.1)
id └─────┘ └─────────────┘ └──────────┘
src └─────┘└─────┘┴ └─────────────┘┴ └──────┘└──────────┘┴ └───
typ └─────┘└─────┘┴ └─────────────┘┴ └──────┘└──────────┘┴ └───
doc └─────┘ ┴ ┴ └──────┘ ┴ └───
txt └─────┘ ┴ ┴ └──────┘ ┴ └───
par └─────┘ ┴ ┴ └──────┘ ┴ └───
pid ┴ ┴ ┴ └──────┘ ┴ └───
st ──────────────────────────────────────────────────────────────
40 (λ _ _ _, mem_univ _)
id └──────┘
src ───┘ └──────┘└──────┘└───
typ ───┘ └──────┘└──────┘└───
doc ───┘ └──────┘ └───
txt ───┘ └──────┘ └───
par ───┘ └──────┘ └───
pid ───┘ └──────┘ └───
st ──────────────────────────
41 (λ a₁ a₂ _ _ _ _ h,
src ───┘ └─────────────────
typ ───┘ └─────────────────
doc ───┘ └─────────────────
txt ───┘ └─────────────────
par ───┘ └─────────────────
pid ───┘ └─────────────────
st ────────────────────────
42 subtype.eq ((mem_fixed_points' α).1 a₂.2 a₁.1 (quotient.exact' h)))
id └────────┘ └───────────────┘ ┴ └─────────────┘
src ─────┘└────────┘┴ └───────────────┘┴ └──┘ └─┘ └─┘ └─────────────┘┴ └───
typ ─────┘└────────┘┴ └───────────────┘┴┴└──┘ └─┘ └─┘ └─────────────┘┴ └───
doc ─────┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ └───
txt ─────┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ └───
par ─────┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ └───
pid ─────┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ └───
st ──────────────────────────────────────────────────────────────────────────
43 (λ b, _)
src ─────┘ └──────
typ ─────┘ └──────
doc ─────┘ └──────
txt ─────┘ └──────
par ─────┘ └──────
pid ─────┘ └──────
st ───────────────
44 (λ a ha _, by rw [← mem_fixed_points_iff_card_orbit_eq_one.1 a.2];
id └────────────────────────────────────┘ ┴
src ─────┘ └───────┘ ┴└────┘└────────────────────────────────────┘└─┘ └─┘└─
typ ─────┘ └───────┘ ┴└────┘└────────────────────────────────────┘└─┘┴└─┘└─
doc ─────┘ └───────┘ ┴└────┘ └─┘ └─┘└─
txt ─────┘ └───────┘ ┴└────┘ └─┘ └─┘└─
par ─────┘ └───────┘ ┴└────┘ └─┘ └─┘└─
pid ─────┘ └───────┘ └─────┘ └─┘ └────
st ──────────────────┘└───────────────────────────────────────────────┘└─┘└─
45 simp only [quotient.eq']; congr)),
id └──────────┘
src ───────┘└─────────┘└──────────┘┴└┘└───┘└┘
typ ───────┘└─────────┘└──────────┘┴└┘└───┘└┘
doc ───────┘└─────────┘ ┴└┘ └┘
txt ───────┘└─────────┘ ┴└┘└───┘└┘
par ───────┘└─────────┘ ┴└┘└───┘└┘
pid ──────────────────┘ └────────┘
st ──────────────────────────────────────┘└┘└─
46 { refine quotient.induction_on' b (λ b _ hb, _),
id └────────────────────┘ ┴
src └─────┘└────────────────────┘┴ ┴ └─────────┘
typ └─────┘└────────────────────┘┴┴┴ └─────────┘
doc └─────┘ ┴ ┴ └─────────┘
txt └─────┘ ┴ ┴ └─────────┘
par └─────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ └─────────┘
st ────────────────────────────────────────────────┘└─
47 have : card (orbit G b) ∣ p ^ n,
id └──┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘└──┘┴ └───┘┴ ┴ └┘┴┴ ┴┴┴
typ └─────┘└──┘┴ └───┘┴┴┴┴└┘┴┴┴┴┴┴┴
doc └─────┘└──┘┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ──────────────────────────────────┘└─
48 { rw [← h, fintype.card_congr (orbit_equiv_quotient_stabilizer G b)];
id ┴ └────────────────┘ └─────────────────────────────┘ ┴ ┴
src └────┘ └┘└────────────────┘┴ └─────────────────────────────┘┴ ┴ └┘
typ └────┘┴└┘└────────────────┘┴ └─────────────────────────────┘┴┴┴┴└┘
doc └────┘ └┘ ┴ ┴ ┴ └┘
txt └────┘ └┘ ┴ ┴ ┴ └┘
par └────┘ └┘ ┴ ┴ ┴ └┘
pid └──┘ └┘ ┴ ┴ ┴ └┘
st ─────┘└─────┘└────────────────────────────────────────────────────────┘┴└─
49 exact card_quotient_dvd_card _ },
id └────────────────────┘
src └────┘└────────────────────┘└─┘
typ └────┘└────────────────────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ────────────────────────────────────┘└┘└
50 rcases (nat.dvd_prime_pow hp).1 this with ⟨k, _, hk⟩,
id └───────────────┘ └┘ └──┘
src └─────┘ └───────────────┘┴ └──┘ └──────────────┘
typ └─────┘ └───────────────┘┴└┘└──┘└──┘└──────────────┘
doc └─────┘ ┴ └──┘ └──────────────┘
txt └─────┘ ┴ └──┘ └──────────────┘
par └─────┘ ┴ └──┘ └──────────────┘
pid ┴ ┴ └──┘ └──────────────┘
st ───────────────────────────────────────────────────────┘└─
51 have hb' :¬ p ^ 1 ∣ p ^ k,
id ┴ ┴
src └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
typ └────────┘ ┴ ┴ └─┘ ┴┴┴ ┴┴
doc └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
txt └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴
pid └──────┘└┘ ┴ ┴ └─┘ ┴ ┴ ┴
st ────────────────────────────┘└─
52 { rw [nat.pow_one, ← hk, ← nat.modeq.modeq_zero_iff, ← zmodp.eq_iff_modeq_nat hp,
id └─────────┘ └┘ └──────────────────────┘ └────────────────────┘ └┘
src └──┘└─────────┘└──┘ └──┘└──────────────────────┘└──┘└────────────────────┘┴ └─
typ └──┘└─────────┘└──┘└┘└──┘└──────────────────────┘└──┘└────────────────────┘┴└┘└─
doc └──┘ └──┘ └──┘ └──┘ ┴ └─
txt └──┘ └──┘ └──┘ └──┘ ┴ └─
par └──┘ └──┘ └──┘ └──┘ ┴ └─
pid └┘ └──┘ └──┘ └──┘ ┴ └─
st ─────┘└─────────────┘└────┘└──────────────────────────┘└───────────────────────────┘└─
53 nat.cast_zero, ← ne.def],
id └───────────┘ └────┘
src ───────┘└───────────┘└──┘└────┘┴
typ ───────┘└───────────┘└──┘└────┘┴
doc ───────┘ └──┘ ┴
txt ───────┘ └──┘ ┴
par ───────┘ └──┘ ┴
pid ───────┘ └──┘ ┴
st ────────────────────┘└────────┘└──
54 exact eq.mpr (by simp only [quotient.eq']; congr) hb },
id └────┘ └──────────┘ └┘
src └────┘└────┘┴ ┴└─────────┘└──────────┘┴└┘└───┘└┘ ┴
typ └────┘└────┘┴ ┴└─────────┘└──────────┘┴└┘└───┘└┘└┘┴
doc └────┘ ┴ ┴└─────────┘ ┴└┘ └┘ ┴
txt └────┘ ┴ ┴└─────────┘ ┴└┘└───┘└┘ ┴
par └────┘ ┴ ┴└─────────┘ ┴└┘└───┘└┘ ┴
pid ┴ ┴ └──────────┘ └────────┘ ┴
st ─────────────────────┘└──────────────────────────────┘└───┘└┘└
55 have : k = 0 := nat.le_zero_iff.1 (nat.le_of_lt_succ (lt_of_not_ge (mt (nat.pow_dvd_pow p) hb'))),
id ┴ ┴ └─────────────┘ └───────────────┘ └──────────┘ └┘ └─────────────┘ ┴ └─┘
src └─────┘ ┴┴└────┘└─────────────┘└─┘ └───────────────┘┴ └──────────┘┴ └┘┴ └─────────────┘┴ └┘ └─┘
typ └─────┘┴┴┴└────┘└─────────────┘└─┘ └───────────────┘┴ └──────────┘┴ └┘┴ └─────────────┘┴┴└┘└─┘└─┘
doc └─────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └─┘
txt └─────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └─┘
par └─────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └─┘
pid └───┘└┘ ┴ ┴└───┘ └─┘ ┴ ┴ ┴ ┴ └┘ └─┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
56 refine ⟨⟨b, mem_fixed_points_iff_card_orbit_eq_one.2 $ by rw [hk, this, nat.pow_zero]⟩, mem_univ _,
id ┴ └────────────────────────────────────┘ └┘ └──┘ └──────────┘ └──────┘
src └─────┘ └┘└────────────────────────────────────┘└─┘ ┴ ┴└──┘ └┘ └┘└──────────┘┴└─┘└──────┘└───
typ └─────┘ ┴└┘└────────────────────────────────────┘└─┘ ┴ ┴└──┘└┘└┘└──┘└┘└──────────┘┴└─┘└──────┘└───
doc └─────┘ └┘ └─┘ ┴ ┴└──┘ └┘ └┘ ┴└─┘ └───
txt └─────┘ └┘ └─┘ ┴ ┴└──┘ └┘ └┘ ┴└─┘ └───
par └─────┘ └┘ └─┘ ┴ ┴└──┘ └┘ └┘ ┴└─┘ └───
pid ┴ └┘ └─┘ ┴ └───┘ └┘ └┘ └──┘ └───
st ────────────────────────────────────────────────────────────┘└─────┘└────┘└────────────┘┴└──────────────
57 by simp [zero_ne_one], rfl⟩ }
id └─────────┘ └─┘
src ─────┘ ┴└────┘└─────────┘┴└┘└─┘└┘
typ ─────┘ ┴└────┘└─────────┘┴└┘└─┘└┘
doc ─────┘ ┴└────┘ ┴└┘ └┘
txt ─────┘ ┴└────┘ ┴└┘ └┘
par ─────┘ ┴└────┘ ┴└┘ └┘
pid ─────┘ └─────┘ └─┘ ┴┴
st ───────┘└─────────────────┘└─────┘└─
58 end
st ──┘
59 ... = _ : by simp; refl
src └──┘ └────
typ └──┘ └────
doc └──┘ └────
txt └──┘ └────
par └──┘ └────
pid └
st └───────────
60
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
61 end mul_action
62
63 lemma quotient_group.card_preimage_mk [fintype G] (s : set G) [is_subgroup s]
id └─────┘ ┴ └─┘ ┴ └─────────┘ ┴
src └─────┘ └─┘ └─────────┘
typ └─────┘ ┴ └─┘ ┴ └─────────┘ ┴
doc └─────┘ └─────────┘
64 (t : set (quotient s)) : fintype.card (quotient_group.mk ⁻¹' t) =
id └─┘ └──────┘ ┴ └──────────┘ └───────────────┘ └─┘ ┴ ┴
src └─┘ └──────┘ └──────────┘ └───────────────┘ └─┘ ┴
typ └─┘ └──────┘ ┴ └──────────┘ └───────────────┘ └─┘ ┴ ┴
doc └──────┘ └──────────┘ └─┘
65 fintype.card s * fintype.card t :=
id └──────────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
66 by rw [← fintype.card_prod, fintype.card_congr
id └───────────────┘ └────────────────┘
src └────┘└───────────────┘└┘└────────────────┘└
typ └────┘└───────────────┘└┘└────────────────┘└
doc └────┘ └┘ └
txt └────┘ └┘ └
par └────┘ └┘ └
pid └──┘ └┘ └
st └──────────────────────┘└────────────────────
67 (preimage_mk_equiv_subgroup_times_set _ _)]
id └──────────────────────────────────┘
src ─┘ └──────────────────────────────────┘└──────
typ ─┘ └──────────────────────────────────┘└──────
doc ─┘ └──────
txt ─┘ └──────
par ─┘ └──────
pid ─┘ └────┘└
st ───────────────────────────────────────────┘┴└
68
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
69 namespace sylow
70
71 def mk_vector_prod_eq_one (n : ℕ) (v : vector G n) : vector G (n+1) :=
id ┴ └────┘ ┴ ┴ └────┘ ┴ ┴┴
src ┴ └────┘ └────┘ ┴
typ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴┴
72 v.to_list.prod⁻¹ :: v
id ┴└──────┘└───┘└┘ └┘ ┴
src └──────┘└───┘└┘ └┘
typ ┴└──────┘└───┘└┘ └┘ ┴
doc └───┘
73
74 lemma mk_vector_prod_eq_one_inj (n : ℕ) : injective (@mk_vector_prod_eq_one G _ n) :=
id ┴ └───────┘ └───────────────────┘ ┴ ┴
src ┴ └───────┘ └───────────────────┘
typ ┴ └───────┘ └───────────────────┘ ┴ ┴
75 λ ⟨v, _⟩ ⟨w, _⟩ h, subtype.eq (show v = w, by injection h with h; injection h)
id ┴┴ ┴┴ ┴ └────────┘ ┴ ┴ ┴
src └────────┘ ┴ └────────┘ └─────┘ └────────┘
typ ┴┴ ┴┴ ┴ └────────┘ ┴ └────────┘┴└─────┘ └────────┘┴
doc └────────┘ └─────┘ └────────┘
txt └────────┘ └─────┘ └────────┘
par └────────┘ └─────┘ └────────┘
pid ┴ └─────┘ ┴
st └──────────────────────────────┘
76
77 def vectors_prod_eq_one (G : Type*) [group G] (n : ℕ) : set (vector G n) :=
id └───┘ ┴ ┴ └─┘ └────┘ ┴ ┴
src └───┘ ┴ └─┘ └────┘
typ └───┘ ┴ ┴ └─┘ └────┘ ┴ ┴
78 {v | v.to_list.prod = 1}
id ┴┴ ┴└──────┘└───┘ ┴
src ┴ └──────┘└───┘ ┴
typ ┴┴ ┴└──────┘└───┘ ┴
doc └───┘
79
80 lemma mem_vectors_prod_eq_one {n : ℕ} (v : vector G n) :
id ┴ └────┘ ┴ ┴
src ┴ └────┘
typ ┴ └────┘ ┴ ┴
81 v ∈ vectors_prod_eq_one G n ↔ v.to_list.prod = 1 := iff.rfl
id ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴└──────┘└───┘ ┴ └─────┘
src ┴ └─────────────────┘ ┴ └──────┘└───┘ ┴ └─────┘
typ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴└──────┘└───┘ ┴ └─────┘
doc └───┘
82
83 lemma mem_vectors_prod_eq_one_iff {n : ℕ} (v : vector G (n + 1)) :
id ┴ └────┘ ┴ ┴ ┴
src ┴ └────┘ ┴
typ ┴ └────┘ ┴ ┴ ┴
84 v ∈ vectors_prod_eq_one G (n + 1) ↔ v ∈ set.range (@mk_vector_prod_eq_one G _ n) :=
id ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └───────────────────┘ ┴ ┴
src ┴ └─────────────────┘ ┴ ┴ ┴ └───────┘ └───────────────────┘
typ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └───────────────────┘ ┴ ┴
doc └───────┘
85 ⟨λ (h : v.to_list.prod = 1), ⟨v.tail,
id ┴└──────┘└───┘ ┴ ┴└───┘
src └──────┘└───┘ ┴ └───┘
typ ┴└──────┘└───┘ ┴ ┴└───┘
doc └───┘
86 begin
st └─────
87 unfold mk_vector_prod_eq_one,
src └──────────────────────────┘
typ └──────────────────────────┘
doc └──────────────────────────┘
txt └──────────────────────────┘
par └──────────────────────────┘
pid └────────────────────┘
st ───────────────────────────────┘└─
88 conv {to_rhs, rw ← vector.cons_head_tail v},
id └───────────────────┘ ┴
src └────┘└────┘└┘└───┘└───────────────────┘┴ ┴
typ └────┘└────┘└┘└───┘└───────────────────┘┴┴┴
txt └────┘└────┘└┘└───┘ ┴ ┴
par └────┘└────┘└┘└───┘ ┴ ┴
pid ┴└────────────┘ ┴ ┴
st ─────────┘└────┘└────────────────────────────┘└┘└
89 suffices : (v.tail.to_list.prod)⁻¹ = v.head,
id └─────────────────┘ └┘ ┴ └────┘
src └─────────┘ └─────────────────┘┴└┘┴┴┴└────┘
typ └─────────┘ └─────────────────┘┴└┘┴┴┴└────┘
doc └─────────┘ └─────────────────┘┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴
pid └───────┘└┘ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
90 { rw this },
id └──┘
src └─┘ ┴
typ └─┘└──┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────┘└──────┘└┘└
91 rw [← mul_right_inj v.tail.to_list.prod, inv_mul_self, ← list.prod_cons,
id └───────────┘ └─────────────────┘ └──────────┘ └────────────┘
src └────┘└───────────┘┴└─────────────────┘└┘└──────────┘└──┘└────────────┘└─
typ └────┘└───────────┘┴└─────────────────┘└┘└──────────┘└──┘└────────────┘└─
doc └────┘ ┴└─────────────────┘└┘ └──┘ └─
txt └────┘ ┴ └┘ └──┘ └─
par └────┘ ┴ └┘ └──┘ └─
pid └──┘ ┴ └┘ └──┘ └─
st ──────────────────────────────────────────┘└────────────┘└────────────────┘└─
92 ← vector.to_list_cons, vector.cons_head_tail, h]
id └─────────────────┘ └───────────────────┘ ┴
src ───────┘└─────────────────┘└┘└───────────────────┘└┘ └─
typ ───────┘└─────────────────┘└┘└───────────────────┘└┘┴└─
doc ───────┘ └┘ └┘ └─
txt ───────┘ └┘ └┘ └─
par ───────┘ └┘ └┘ └─
pid ───────┘ └┘ └┘ ┴└
st ──────────────────────────┘└─────────────────────┘└─┘┴└
93 end⟩,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
94 λ ⟨w, hw⟩, by rw [mem_vectors_prod_eq_one, ← hw, mk_vector_prod_eq_one,
id ┴ └─────────────────────┘ └┘ └───────────────────┘
src └──┘└─────────────────────┘└──┘ └┘└───────────────────┘└─
typ ┴ └──┘└─────────────────────┘└──┘└┘└┘└───────────────────┘└─
doc └──┘ └──┘ └┘ └─
txt └──┘ └──┘ └┘ └─
par └──┘ └──┘ └┘ └─
pid └┘ └──┘ └┘ └─
st └──────────────────────────┘└────┘└─────────────────────┘└─
95 vector.to_list_cons, list.prod_cons, inv_mul_self]⟩
id └─────────────────┘ └────────────┘ └──────────┘
src ───┘└─────────────────┘└┘└────────────┘└┘└──────────┘┴
typ ───┘└─────────────────┘└┘└────────────┘└┘└──────────┘┴
doc ───┘ └┘ └┘ ┴
txt ───┘ └┘ └┘ ┴
par ───┘ └┘ └┘ ┴
pid ───┘ └┘ └┘ ┴
st ──────────────────────┘└──────────────┘└────────────┘┴
96
97 def rotate_vectors_prod_eq_one (G : Type*) [group G] (n : ℕ+) (m : multiplicative (zmod n))
id └───┘ ┴ └┘ └────────────┘ └──┘ ┴
src └───┘ └┘ └────────────┘ └──┘
typ └───┘ ┴ └┘ └────────────┘ └──┘ ┴
doc └┘
98 (v : vectors_prod_eq_one G n) : vectors_prod_eq_one G n :=
id └─────────────────┘ ┴ ┴ └─────────────────┘ ┴ ┴
src └─────────────────┘ └─────────────────┘
typ └─────────────────┘ ┴ ┴ └─────────────────┘ ┴ ┴
99 ⟨⟨v.1.to_list.rotate m.1, by simp⟩, prod_rotate_eq_one_of_prod_eq_one v.2 _⟩
id ┴┴ └─────┘ └────┘ ┴┴ └───────────────────────────────┘ ┴┴
src ┴ └─────┘ └────┘ ┴ └──┘ └───────────────────────────────┘ ┴
typ ┴┴ └─────┘ └────┘ ┴┴ └──┘ └───────────────────────────────┘ ┴┴
doc └────┘ └──┘
txt └──┘
par └──┘
st └───┘
100
101 instance rotate_vectors_prod_eq_one.mul_action (n : ℕ+) :
id └┘
src └┘
typ └┘
doc └┘
102 mul_action (multiplicative (zmod n)) (vectors_prod_eq_one G n) :=
id └────────┘ └────────────┘ └──┘ ┴ └─────────────────┘ ┴ ┴
src └────────┘ └────────────┘ └──┘ └─────────────────┘
typ └────────┘ └────────────┘ └──┘ ┴ └─────────────────┘ ┴ ┴
doc └────────┘
103 { smul := (rotate_vectors_prod_eq_one G n),
id └────────────────────────┘ ┴ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴ ┴
104 one_smul := λ v, subtype.eq $ vector.eq _ _ $ rotate_zero v.1.to_list,
id ┴ └────────┘ └───────┘ └─────────┘ ┴┴ └─────┘
src └────────┘ └───────┘ └─────────┘ ┴ └─────┘
typ ┴ └────────┘ └───────┘ └─────────┘ ┴┴ └─────┘
105 mul_smul := λ a b ⟨⟨v, hv₁⟩, hv₂⟩, subtype.eq $ vector.eq _ _ $
id ┴ ┴ ┴ ┴ └────────┘ └───────┘
src └────────┘ └───────┘
typ ┴ ┴ ┴ ┴ └────────┘ └───────┘
106 show v.rotate ((a + b : zmod n).val) = list.rotate (list.rotate v (b.val)) (a.val),
id └─────┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ └─────────┘ └─────────┘ ┴└──┘ ┴└──┘
src └─────┘ ┴ └──┘ └─┘ ┴ └─────────┘ └─────────┘ └──┘ └──┘
typ └─────┘ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ └─────────┘ └─────────┘ ┴└──┘ ┴└──┘
doc └─────┘ └─────────┘ └─────────┘
107 by rw [zmod.add_val, rotate_rotate, ← rotate_mod _ (b.1 + a.1), add_comm, hv₁] }
id └──────────┘ └───────────┘ └────────┘ ┴ ┴ ┴ └──────┘ └─┘
src └──┘└──────────┘└┘└───────────┘└──┘└────────┘└─┘ └─┘┴┴ └───┘└──────┘└┘ └┘
typ └──┘└──────────┘└┘└───────────┘└──┘└────────┘└─┘ ┴└─┘┴┴┴└───┘└──────┘└┘└─┘└┘
doc └──┘ └┘ └──┘ └─┘ └─┘ ┴ └───┘ └┘ └┘
txt └──┘ └┘ └──┘ └─┘ └─┘ ┴ └───┘ └┘ └┘
par └──┘ └┘ └──┘ └─┘ └─┘ ┴ └───┘ └┘ └┘
pid └┘ └┘ └──┘ └─┘ └─┘ ┴ └───┘ └┘ ┴┴
st └───────────────┘└─────────────┘└──────────────────────────┘└────────┘└───┘┴┴
108
109 lemma one_mem_vectors_prod_eq_one (n : ℕ) : vector.repeat (1 : G) n ∈ vectors_prod_eq_one G n :=
id ┴ └───────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
src ┴ └───────────┘ ┴ └─────────────────┘
typ ┴ └───────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
110 by simp [vector.repeat, vectors_prod_eq_one]
id └───────────┘ └─────────────────┘
src └────┘└───────────┘└┘└─────────────────┘└─
typ └────┘└───────────┘└┘└─────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────────────────────
111
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
112 lemma one_mem_fixed_points_rotate (n : ℕ+) :
id └┘
src └┘
typ └┘
doc └┘
113 (⟨vector.repeat (1 : G) n, one_mem_vectors_prod_eq_one n⟩ : vectors_prod_eq_one G n) ∈
id └───────────┘ ┴ ┴ └─────────────────────────┘ ┴ └─────────────────┘ ┴ ┴ ┴
src └───────────┘ └─────────────────────────┘ └─────────────────┘ ┴
typ └───────────┘ ┴ ┴ └─────────────────────────┘ ┴ └─────────────────┘ ┴ ┴ ┴
114 fixed_points (multiplicative (zmod n)) (vectors_prod_eq_one G n) :=
id └──────────┘ └────────────┘ └──┘ ┴ └─────────────────┘ ┴ ┴
src └──────────┘ └────────────┘ └──┘ └─────────────────┘
typ └──────────┘ └────────────┘ └──┘ ┴ └─────────────────┘ ┴ ┴
115 λ m, subtype.eq $ vector.eq _ _ $
id ┴ └────────┘ └───────┘
src └────────┘ └───────┘
typ ┴ └────────┘ └───────┘
116 by haveI : nonempty G := ⟨1⟩; exact
id └──────┘ ┴
src └──────┘└──────┘┴ └──┘ └┘ └────┘
typ └──────┘└──────┘┴┴└──┘ └┘ └────┘
doc └──────┘ ┴ └──┘ └┘ └────┘
txt └──────┘ ┴ └──┘ └┘ └────┘
par └──────┘ ┴ └──┘ └┘ └────┘
pid ┴└┘ ┴ └──┘ └┘ ┴
st └─────────────────────────────────
117 rotate_eq_self_iff_eq_repeat.2 ⟨(1 : G),
id └──────────────────────────┘
src └──────────────────────────┘└─┘ └──┘ └──
typ └──────────────────────────┘└─┘ └──┘ └──
doc └─┘ └──┘ └──
txt └─┘ └──┘ └──
par └─┘ └──┘ └──
pid └─┘ └──┘ └──
st ─────────────────────────────────────────
118 show list.repeat (1 : G) n = list.repeat 1 (list.repeat (1 : G) n).length, by simp⟩ _
id ┴ └─────────┘ ┴ ┴
src ─┘ ┴ ┴ └──┘ └┘ ┴┴┴ └─┘ └─────────┘┴ └──┘ └┘ └───────────┘└──┘└───
typ ─┘ ┴ ┴ └──┘ └┘ ┴┴┴ └─┘ └─────────┘┴ └──┘┴└┘┴└───────────┘└──┘└───
doc ─┘ ┴ ┴ └──┘ └┘ ┴ ┴ └─┘ ┴ └──┘ └┘ └───────────┘└──┘└───
txt ─┘ ┴ ┴ └──┘ └┘ ┴ ┴ └─┘ ┴ └──┘ └┘ └───────────┘└──┘└───
par ─┘ ┴ ┴ └──┘ └┘ ┴ ┴ └─┘ ┴ └──┘ └┘ └───────────┘└──┘└───
pid ─┘ ┴ ┴ └──┘ └┘ ┴ ┴ └─┘ ┴ └──┘ └┘ └──────────────────┘└
st ──────────────────────────────────────────────────────────────────────────────┘└───┘└───
119
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
120 /-- Cauchy's theorem -/
121 lemma exists_prime_order_of_dvd_card [fintype G] {p : ℕ} (hp : nat.prime p)
id └─────┘ ┴ ┴ └───────┘ ┴
src └─────┘ ┴ └───────┘
typ └─────┘ ┴ ┴ └───────┘ ┴
doc └─────┘ └───────┘
122 (hdvd : p ∣ card G) : ∃ x : G, order_of x = p :=
id ┴ ┴ └──┘ ┴ ┴ ┴┴ └──────┘ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ └──────┘ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴┴ └──────┘ ┴ ┴ ┴
doc └──┘ └──────┘
123 let n : ℕ+ := ⟨p - 1, nat.sub_pos_of_lt hp.one_lt⟩ in
id └┘ ┴ ┴ └───────────────┘ └┘└─────┘
src └┘ ┴ └───────────────┘ └─────┘
typ └┘ ┴ ┴ └───────────────┘ └┘└─────┘
doc └┘
124 let p' : ℕ+ := ⟨p, hp.pos⟩ in
id └┘ ┴ └┘└──┘
src └┘ └──┘
typ └┘ ┴ └┘└──┘
doc └┘
125 have hn : p' = n + 1 := subtype.eq (nat.succ_sub hp.pos),
id └┘ ┴ ┴ ┴ └────────┘ └──────────┘ └┘└──┘
src ┴ ┴ └────────┘ └──────────┘ └──┘
typ └┘ ┴ ┴ ┴ └────────┘ └──────────┘ └┘└──┘
126 have hcard : card (vectors_prod_eq_one G (n + 1)) = card G ^ (n : ℕ),
id └──┘ └─────────────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘ └─────────────────┘ ┴ ┴ └──┘ ┴ ┴
typ └──┘ └─────────────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘
127 by rw [set.ext mem_vectors_prod_eq_one_iff,
id └─────┘ └─────────────────────────┘
src └──┘└─────┘┴└─────────────────────────┘└─
typ └──┘└─────┘┴└─────────────────────────┘└─
doc └──┘ ┴ └─
txt └──┘ ┴ └─
par └──┘ ┴ └─
pid └┘ ┴ └─
st └──────────────────────────────────────┘└─
128 set.card_range_of_injective (mk_vector_prod_eq_one_inj _), card_vector],
id └─────────────────────────┘ └───────────────────────┘ └─────────┘
src ───┘└─────────────────────────┘┴ └───────────────────────┘└───┘└─────────┘┴
typ ───┘└─────────────────────────┘┴ └───────────────────────┘└───┘└─────────┘┴
doc ───┘ ┴ └───┘ ┴
txt ───┘ ┴ └───┘ ┴
par ───┘ ┴ └───┘ ┴
pid ───┘ ┴ └───┘ ┴
st ────────────────────────────────────────────────────────────┘└───────────┘┴
129 have hzmod : fintype.card (multiplicative (zmod p')) =
id └──────────┘ └────────────┘ └──┘ └┘ ┴
src └──────────┘ └────────────┘ └──┘ ┴
typ └──────────┘ └────────────┘ └──┘ └┘ ┴
doc └──────────┘
130 (p' : ℕ) ^ 1 := (nat.pow_one p').symm ▸ card_fin _,
id └┘ ┴ ┴ └─────────┘ └┘ └──┘ ┴ └──────┘
src ┴ ┴ └─────────┘ └──┘ ┴ └──────┘
typ └┘ ┴ ┴ └─────────┘ └┘ └──┘ ┴ └──────┘
131 have hmodeq : _ = _ := @mul_action.card_modeq_card_fixed_points
id ┴ └─────────────────────────────────────┘
src ┴ └─────────────────────────────────────┘
typ ┴ └─────────────────────────────────────┘
132 (multiplicative (zmod p')) (vectors_prod_eq_one G p') _ _ _ _ _ _ 1 hp hzmod,
id └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘ └┘ └───┘
src └────────────┘ └──┘ └─────────────────┘
typ └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘ └┘ └───┘
133 have hdvdcard : p ∣ fintype.card (vectors_prod_eq_one G (n + 1)) :=
id ┴ ┴ └──────────┘ └─────────────────┘ ┴ ┴ ┴
src ┴ └──────────┘ └─────────────────┘ ┴
typ ┴ ┴ └──────────┘ └─────────────────┘ ┴ ┴ ┴
doc └──────────┘
134 calc p ∣ card G ^ 1 : by rwa nat.pow_one
id ┴ └──┘ ┴ ┴ └─────────┘
src └──┘ ┴ └──┘└─────────┘└
typ ┴ └──┘ ┴ ┴ └──┘└─────────┘└
doc └──┘ └──┘ └
txt └──┘ └
par └──┘ └
pid ┴ └
st └────────────────
135 ... ∣ card G ^ (n : ℕ) : nat.pow_dvd_pow _ n.2
id └──┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴┴
src ─┘ └──┘ ┴ ┴ └─────────────┘ ┴
typ ─┘ └──┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴┴
doc ─┘ └──┘
txt ─┘
par ─┘
pid ─┘
st ─┘
136 ... = card (vectors_prod_eq_one G (n + 1)) : hcard.symm,
id └──┘ └─────────────────┘ ┴ ┴ ┴ └───┘└───┘
src └──┘ └─────────────────┘ ┴ └───┘
typ └──┘ └─────────────────┘ ┴ ┴ ┴ └───┘└───┘
doc └──┘
137 have hdvdcard₂ : p ∣ card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) :=
id ┴ ┴ └──┘ └──────────┘ └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘
src ┴ └──┘ └──────────┘ └────────────┘ └──┘ └─────────────────┘
typ ┴ ┴ └──┘ └──────────┘ └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘
doc └──┘
138 nat.dvd_of_mod_eq_zero (hmodeq ▸ hn.symm ▸ nat.mod_eq_zero_of_dvd hdvdcard),
id └────────────────────┘ └────┘ ┴ └┘└───┘ ┴ └────────────────────┘ └──────┘
src └────────────────────┘ ┴ └───┘ ┴ └────────────────────┘
typ └────────────────────┘ └────┘ ┴ └┘└───┘ ┴ └────────────────────┘ └──────┘
139 have hcard_pos : 0 < card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) :=
id ┴ └──┘ └──────────┘ └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘
src ┴ └──┘ └──────────┘ └────────────┘ └──┘ └─────────────────┘
typ ┴ └──┘ └──────────┘ └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘
doc └──┘
140 fintype.card_pos_iff.2 ⟨⟨⟨vector.repeat 1 p', one_mem_vectors_prod_eq_one _⟩,
id └──────────────────┘┴ └───────────┘ └┘ └─────────────────────────┘
src └──────────────────┘┴ └───────────┘ └─────────────────────────┘
typ └──────────────────┘┴ └───────────┘ └┘ └─────────────────────────┘
141 one_mem_fixed_points_rotate _⟩⟩,
id └─────────────────────────┘
src └─────────────────────────┘
typ └─────────────────────────┘
142 have hlt : 1 < card (fixed_points (multiplicative (zmod p')) (vectors_prod_eq_one G p')) :=
id ┴ └──┘ └──────────┘ └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘
src ┴ └──┘ └──────────┘ └────────────┘ └──┘ └─────────────────┘
typ ┴ └──┘ └──────────┘ └────────────┘ └──┘ └┘ └─────────────────┘ ┴ └┘
doc └──┘
143 calc (1 : ℕ) < p' : hp.one_lt
id ┴ └┘ └┘└─────┘
src ┴ └─────┘
typ ┴ └┘ └┘└─────┘
144 ... ≤ _ : nat.le_of_dvd hcard_pos hdvdcard₂,
id └───────────┘ └───────┘ └───────┘
src └───────────┘
typ └───────────┘ └───────┘ └───────┘
145 let ⟨⟨⟨⟨x, hx₁⟩, hx₂⟩, hx₃⟩, hx₄⟩ := fintype.exists_ne_of_one_lt_card hlt
id └─┘ ┴ └─┘ └─┘ └──────────────────────────────┘ └─┘
src └──────────────────────────────┘
typ └─┘ ┴ └─┘ └─┘ └──────────────────────────────┘ └─┘
146 ⟨_, one_mem_fixed_points_rotate p'⟩ in
id └─────────────────────────┘ └┘
src └─────────────────────────┘
typ └─────────────────────────┘ └┘
147 have hx : x ≠ list.repeat (1 : G) p', from λ h, by simpa [h, vector.repeat] using hx₄,
id ┴ └─────────┘ ┴ └┘ ┴ ┴ └───────────┘ └─┘
src ┴ └─────────┘ └─────┘ └┘└───────────┘└──────┘
typ ┴ └─────────┘ ┴ └┘ ┴ └─────┘┴└┘└───────────┘└──────┘└─┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st └─────────────────────────────────┘
148 have nG : nonempty G, from ⟨1⟩,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
149 have ∃ a, x = list.repeat a x.length := by exactI rotate_eq_self_iff_eq_repeat.1 (λ n,
id ┴ ┴┴ ┴ └─────────┘ ┴ └─────┘ └──────────────────────────┘
src ┴ ┴ ┴ └─────────┘ └─────┘ └─────┘└──────────────────────────┘└─┘ └───
typ ┴ ┴┴ ┴ └─────────┘ ┴ └─────┘ └─────┘└──────────────────────────┘└─┘ └───
doc └─────┘ └─┘ └───
txt └─────┘ └─┘ └───
par └─────┘ └─┘ └───
pid ┴ └─┘ └───
st └────────────────────────────────────────────
150 have list.rotate x (n : zmod p').val = x :=
id ┴ ┴
src ─┘ └───────────┘ ┴ └─┘ ┴ └────┘┴┴ └───
typ ─┘ └───────────┘ ┴ └─┘ ┴ └────┘┴┴┴└───
doc ─┘ └───────────┘ ┴ └─┘ ┴ └────┘ ┴ └───
txt ─┘ └───────────┘ ┴ └─┘ ┴ └────┘ ┴ └───
par ─┘ └───────────┘ ┴ └─┘ ┴ └────┘ ┴ └───
pid ─┘ └───────────┘ ┴ └─┘ ┴ └────┘ ┴ └───
st ──────────────────────────────────────────────
151 subtype.mk.inj (subtype.mk.inj (hx₃ (n : zmod p'))),
id └────────────┘ └─┘ └──┘ └┘
src ───┘ ┴ └────────────┘┴ ┴ └─┘└──┘┴ └────
typ ───┘ ┴ └────────────┘┴ └─┘┴ └─┘└──┘┴└┘└────
doc ───┘ ┴ ┴ ┴ └─┘ ┴ └────
txt ───┘ ┴ ┴ ┴ └─┘ ┴ └────
par ───┘ ┴ ┴ ┴ └─┘ ┴ └────
pid ───┘ ┴ ┴ ┴ └─┘ ┴ └────
st ─────────────────────────────────────────────────────────
152 by rwa [zmod.val_cast_nat, ← hx₁, rotate_mod] at this),
id └───────────────┘ └─┘ └────────┘
src ─┘ ┴└───┘└───────────────┘└──┘ └┘└────────┘└───────┘┴
typ ─┘ ┴└───┘└───────────────┘└──┘└─┘└┘└────────┘└───────┘┴
doc ─┘ ┴└───┘ └──┘ └┘ └───────┘┴
txt ─┘ ┴└───┘ └──┘ └┘ └───────┘┴
par ─┘ ┴└───┘ └──┘ └┘ └───────┘┴
pid ─┘ └────┘ └──┘ └┘ └────────┘
st ───┘└─────────────────────┘└─────┘└──────────┘┴└──────┘┴
153 let ⟨a, ha⟩ := this in
id └─┘ ┴ └┘ └──┘
typ └─┘ ┴ └┘ └──┘
154 ⟨a, have hx1 : x.prod = 1 := hx₂,
id └───┘ ┴
src └───┘ ┴
typ └───┘ ┴
doc └───┘
155 have ha1: a ≠ 1, from λ h, hx (ha.symm ▸ h ▸ hx₁ ▸ rfl),
id ┴ ┴ └┘ └───┘ ┴ ┴ ┴ ┴ └─┘
src ┴ └───┘ ┴ ┴ ┴ └─┘
typ ┴ ┴ └┘ └───┘ ┴ ┴ ┴ ┴ └─┘
156 have a ^ p = 1, by rwa [ha, list.prod_repeat, hx₁] at hx1,
id ┴ ┴ ┴ └┘ └──────────────┘ └─┘
src ┴ ┴ └───┘ └┘└──────────────┘└┘ └──────┘
typ ┴ ┴ ┴ └───┘└┘└┘└──────────────┘└┘└─┘└──────┘
doc └───┘ └┘ └┘ └──────┘
txt └───┘ └┘ └┘ └──────┘
par └───┘ └┘ └┘ └──────┘
pid └┘ └┘ └┘ ┴└─────┘
st └──────┘└────────────────┘└───┘┴└─────┘
157 (hp.2 _ (order_of_dvd_of_pow_eq_one this)).resolve_left
id └┘┴ └────────────────────────┘ └──┘ └──────────┘
src ┴ └────────────────────────┘ └──────────┘
typ └┘┴ └────────────────────────┘ └──┘ └──────────┘
158 (λ h, ha1 (order_of_eq_one_iff.1 h))⟩
id ┴ └─┘ └─────────────────┘┴ ┴
src └─────────────────┘┴
typ ┴ └─┘ └─────────────────┘┴ ┴
159
160 open is_subgroup is_submonoid is_group_hom mul_action
161
162 lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : set G} [is_subgroup H] [fintype H]
id └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
src └─┘ └─────────┘ └─────┘
typ └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
doc └─────────┘ └─────┘
163 {x : G} : (x : quotient H) ∈ fixed_points H (quotient H) ↔ x ∈ normalizer H :=
id ┴ ┴ └──────┘ ┴ ┴ └──────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
src └──────┘ ┴ └──────────┘ └──────┘ ┴ ┴ └────────┘
typ ┴ ┴ └──────┘ ┴ ┴ └──────────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └──────┘ └──────┘
164 ⟨λ hx, have ha : ∀ {y : quotient H}, y ∈ orbit H (x : quotient H) → y = x,
id └┘ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └───┘ └──────┘ ┴
typ └┘ └──────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
165 from λ _, ((mem_fixed_points' _).1 hx _),
id ┴ └───────────────┘ ┴ └┘
src └───────────────┘ ┴
typ ┴ └───────────────┘ ┴ └┘
166 (inv_mem_iff _).1 (mem_normalizer_fintype (λ n hn,
id └─────────┘ ┴ └────────────────────┘ ┴ └┘
src └─────────┘ ┴ └────────────────────┘
typ └─────────┘ ┴ └────────────────────┘ ┴ └┘
167 have (n⁻¹ * x)⁻¹ * x ∈ H := quotient_group.eq.1 (ha (mem_orbit _ ⟨n⁻¹, inv_mem hn⟩)),
id ┴└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────────────┘┴ └┘ └───────┘ ┴└┘ └─────┘ └┘
src └┘ ┴ └┘ ┴ ┴ └───────────────┘┴ └───────┘ └┘ └─────┘
typ ┴└┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────────────┘┴ └┘ └───────┘ ┴└┘ └─────┘ └┘
168 by simpa only [mul_inv_rev, inv_inv] using this)),
id └─────────┘ └─────┘ └──┘
src └──────────┘└─────────┘└┘└─────┘└──────┘
typ └──────────┘└─────────┘└┘└─────┘└──────┘└──┘
doc └──────────┘ └┘ └──────┘
txt └──────────┘ └┘ └──────┘
par └──────────┘ └┘ └──────┘
pid ┴└──┘└┘ └┘ ┴┴└────┘
st └───────────────────────────────────────────┘
169 λ (hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴
src ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴
170 (mem_fixed_points' _).2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.eq.2
id └───────────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └┘ └───────────────┘┴
src └───────────────┘ ┴ └────────────────────┘ └───────────────┘┴
typ └───────────────┘ ┴ ┴ └────────────────────┘ ┴ ┴ └┘ └───────────────┘┴
171 (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy in
id └─┘ ┴ └─┘ └─┘ └┘
typ └─┘ ┴ └─┘ └─┘ └┘
172 have hb₂ : (b * x)⁻¹ * y ∈ H := quotient_group.eq.1 hb₂,
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────────────┘┴
src ┴ └┘ ┴ ┴ └───────────────┘┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────────────┘┴
173 (inv_mem_iff H).1 $ (hx _).2 $ (mul_mem_cancel_right H (inv_mem hb₁)).1
id └─────────┘ ┴ ┴ └┘ ┴ └──────────────────┘ ┴ └─────┘ ┴
src └─────────┘ ┴ ┴ └──────────────────┘ └─────┘ ┴
typ └─────────┘ ┴ ┴ └┘ ┴ └──────────────────┘ ┴ └─────┘ ┴
174 $ by rw hx at hb₂;
id └┘
src └─┘ └─────┘
typ └─┘└┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st └──────────────
175 simpa [mul_inv_rev, mul_assoc] using hb₂)⟩
id └─────────┘ └───────┘ └─┘
src └─────┘└─────────┘└┘└───────┘└──────┘
typ └─────┘└─────────┘└┘└───────┘└──────┘└─┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st ───────────────────────────────────────────┘
176
177 def fixed_points_mul_left_cosets_equiv_quotient (H : set G) [is_subgroup H] [fintype H] :
id └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
src └─┘ └─────────┘ └─────┘
typ └─┘ ┴ └─────────┘ ┴ └─────┘ ┴
doc └─────────┘ └─────┘
178 fixed_points H (quotient H) ≃ quotient (subtype.val ⁻¹' H : set (normalizer H)) :=
id └──────────┘ ┴ └──────┘ ┴ ┴ └──────┘ └─────────┘ └─┘ ┴ └─┘ └────────┘ ┴
src └──────────┘ └──────┘ ┴ └──────┘ └─────────┘ └─┘ └─┘ └────────┘
typ └──────────┘ ┴ └──────┘ ┴ ┴ └──────┘ └─────────┘ └─┘ ┴ └─┘ └────────┘ ┴
doc └──────┘ ┴ └──────┘ └─┘
179 @subtype_quotient_equiv_quotient_subtype G (normalizer H) (id _) (id _) (fixed_points _ _)
id └─────────────────────────────────────┘ ┴ └────────┘ ┴ └┘ └┘ └──────────┘
src └─────────────────────────────────────┘ └────────┘ └┘ └┘ └──────────┘
typ └─────────────────────────────────────┘ ┴ └────────┘ ┴ └┘ └┘ └──────────┘
180 (λ a, mem_fixed_points_mul_left_cosets_iff_mem_normalizer.symm) (by intros; refl)
id ┴ └─────────────────────────────────────────────────┘└───┘
src └─────────────────────────────────────────────────┘└───┘ └────┘ └──┘
typ ┴ └─────────────────────────────────────────────────┘└───┘ └────┘ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
st └───────────┘
181
182 local attribute [instance] set_fintype
id └─────────┘
src └─────────┘
typ └─────────┘
183
184 lemma exists_subgroup_card_pow_prime [fintype G] {p : ℕ} : ∀ {n : ℕ} (hp : nat.prime p)
id └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
src └─────┘ ┴ ┴ └───────┘
typ └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
doc └─────┘ └───────┘
185 (hdvd : p ^ n ∣ card G), ∃ H : set G, is_subgroup H ∧ fintype.card H = p ^ n
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴┴ └─────────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ └─┘ ┴ └─────────┘ ┴ └──────────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─┘ ┴┴ └─────────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────────┘ └──────────┘
186 | 0 := λ _ _, ⟨trivial G, by apply_instance, by simp⟩
id ┴ ┴ └─────┘ ┴
src └─────┘ └────────────┘ └──┘
typ ┴ ┴ └─────┘ ┴ └────────────┘ └──┘
doc └─────┘ └────────────┘ └──┘
txt └────────────┘ └──┘
par └────────────┘ └──┘
st └─────────────┘ └───┘
187 | (n+1) := λ hp hdvd,
id ┴ └┘ └──┘
src ┴
typ ┴ └┘ └──┘
188 let ⟨H, ⟨hH1, hH2⟩⟩ := exists_subgroup_card_pow_prime hp
id └─┘ └────────────────────────────┘ └┘
typ └─┘ └────────────────────────────┘ └┘
189 (dvd.trans (nat.pow_dvd_pow _ (nat.le_succ _)) hdvd) in
id └───────┘ └─────────────┘ └─────────┘ └──┘
src └───────┘ └─────────────┘ └─────────┘
typ └───────┘ └─────────────┘ └─────────┘ └──┘
190 let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd in
id └─┘ └───────────────────────┘ └──┘
src └───────────────────────┘
typ └─┘ └───────────────────────┘ └──┘
191 by exactI
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴
st └───────
192 have hcard : card (quotient H) = s * p :=
id ┴ ┴
src └───────┘ ┴ ┴ └┘┴┴ ┴┴┴ └───
typ └───────┘ ┴ ┴ └┘┴┴ ┴┴┴ └───
doc └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───
txt └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───
par └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───
pid └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───
st ──────────────────────────────────────────
193 (nat.mul_right_inj (show card H > 0, from fintype.card_pos_iff.2
id └───────────────┘ └──┘ ┴ └──────────────────┘
src ─┘ └───────────────┘┴ ┴└──┘┴ ┴┴└───────┘└──────────────────┘└──
typ ─┘ └───────────────┘┴ ┴└──┘┴ ┴┴└───────┘└──────────────────┘└──
doc ─┘ ┴ ┴└──┘┴ ┴ └───────┘ └──
txt ─┘ ┴ ┴ ┴ ┴ └───────┘ └──
par ─┘ ┴ ┴ ┴ ┴ └───────┘ └──
pid ─┘ ┴ ┴ ┴ ┴ └───────┘ └──
st ───────────────────────────────────────────────────────────────────
194 ⟨⟨1, is_submonoid.one_mem H⟩⟩)).1
id └──────────────────┘ ┴
src ─────┘ └─┘└──────────────────┘┴ └──────
typ ─────┘ └─┘└──────────────────┘┴┴└──────
doc ─────┘ └─┘ ┴ └──────
txt ─────┘ └─┘ ┴ └──────
par ─────┘ └─┘ ┴ └──────
pid ─────┘ └─┘ ┴ └──────
st ────────────────────────────────────────
195 (by rwa [← card_eq_card_quotient_mul_card_subgroup, hH2, hs,
id └─────────────────────────────────────┘ └─┘ └┘
src ───┘ ┴└─────┘└─────────────────────────────────────┘└┘ └┘ └─
typ ───┘ ┴└─────┘└─────────────────────────────────────┘└┘└─┘└┘└┘└─
doc ───┘ ┴└─────┘ └┘ └┘ └─
txt ───┘ ┴└─────┘ └┘ └┘ └─
par ───┘ ┴└─────┘ └┘ └┘ └─
pid ───┘ └──────┘ └┘ └┘ └─
st ──────┘└─────────────────────────────────────────────┘└───┘└──┘└─
196 nat.pow_succ, mul_assoc, mul_comm p]),
id └──────────┘ └───────┘ └──────┘ ┴
src ─────┘└──────────┘└┘└───────┘└┘└──────┘┴ ┴└─┘
typ ─────┘└──────────┘└┘└───────┘└┘└──────┘┴┴┴└─┘
doc ─────┘ └┘ └┘ ┴ ┴└─┘
txt ─────┘ └┘ └┘ ┴ ┴└─┘
par ─────┘ └┘ └┘ ┴ ┴└─┘
pid ─────┘ └┘ └┘ ┴ └──┘
st ─────────────────┘└─────────┘└──────────┘┴└──
197 have hm : s * p % p = card (quotient (subtype.val ⁻¹' H : set (normalizer H))) % p :=
id ┴ ┴ └─┘
src └────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴└─┘┴ └─┘ ┴ ┴ └──┘ ┴ └───
typ └────┘┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴└─┘┴ └─┘ ┴ ┴ └──┘ ┴ └───
doc └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─┘┴ └─┘ ┴ ┴ └──┘ ┴ └───
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └───
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └───
pid └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └───
st ──────────────────────────────────────────────────────────────────────────────────────
198 card_congr (fixed_points_mul_left_cosets_equiv_quotient H) ▸ hcard ▸
id └────────┘ └─────────────────────────────────────────┘ ┴
src ─┘└────────┘┴ └─────────────────────────────────────────┘┴ └┘┴┴ ┴ └
typ ─┘└────────┘┴ └─────────────────────────────────────────┘┴ └┘┴┴ ┴ └
doc ─┘ ┴ ┴ └┘ ┴ ┴ └
txt ─┘ ┴ ┴ └┘ ┴ ┴ └
par ─┘ ┴ ┴ └┘ ┴ ┴ └
pid ─┘ ┴ ┴ └┘ ┴ ┴ └
st ───────────────────────────────────────────────────────────────────────
199 card_modeq_card_fixed_points hp hH2,
id └──────────────────────────┘ └┘ └─┘
src ───┘└──────────────────────────┘┴ ┴ └┘
typ ───┘└──────────────────────────┘┴└┘┴└─┘└┘
doc ───┘ ┴ ┴ └┘
txt ───┘ ┴ ┴ └┘
par ───┘ ┴ ┴ └┘
pid ───┘ ┴ ┴ └┘
st ─────────────────────────────────────────
200 have hm' : p ∣ card (quotient (subtype.val ⁻¹' H : set (normalizer H))) :=
id ┴ └──────┘
src └─────┘ ┴┴┴ ┴ └──────┘┴ ┴ ┴ └─┘ ┴ ┴ └──────
typ └─────┘ ┴┴┴ ┴ └──────┘┴ ┴ ┴ └─┘ ┴ ┴ └──────
doc └─────┘ ┴ ┴ ┴ └──────┘┴ ┴ ┴ └─┘ ┴ ┴ └──────
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────
pid └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────
st ───────────────────────────────────────────────────────────────────────────
201 nat.dvd_of_mod_eq_zero
id └────────────────────┘
src ─┘└────────────────────┘└
typ ─┘└────────────────────┘└
doc ─┘ └
txt ─┘ └
par ─┘ └
pid ─┘ └
st ─────────────────────────
202 (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm),
id └────────────────────┘ └──────────┘ └─────┘
src ───┘ ┴└───┘└────────────────────┘┴ └──────────┘└─────┘└─────┘└─────┘└─┘
typ ───┘ ┴└───┘└────────────────────┘┴ └──────────┘└─────┘└─────┘└─────┘└─┘
doc ───┘ ┴└───┘ ┴ └─────┘ └─────┘└─┘
txt ───┘ ┴└───┘ ┴ └─────┘ └─────┘└─┘
par ───┘ ┴└───┘ ┴ └─────┘ └─────┘└─┘
pid ───┘ └────┘ ┴ └─────┘ └────────┘
st ──────┘└─────────────────────────────────────────────┘└───────┘┴└────┘└──
203 let ⟨x, hx⟩ := @exists_prime_order_of_dvd_card _ (quotient_group.group _) _ _ hp hm' in
id ┴ └────────────────────────────┘ └──────────────────┘
src ┴ └┘ └───┘ └────────────────────────────┘└─┘ └──────────────────┘└──────┘ ┴ └──┘
typ ┴ ┴└┘ └───┘ └────────────────────────────┘└─┘ └──────────────────┘└──────┘ ┴ └──┘
doc ┴ └┘ └───┘ └────────────────────────────┘└─┘ └──────┘ ┴ └──┘
txt ┴ └┘ └───┘ └─┘ └──────┘ ┴ └──┘
par ┴ └┘ └───┘ └─┘ └──────┘ ┴ └──┘
pid ┴ └┘ └───┘ └─┘ └──────┘ ┴ └──┘
st ────────────────────────────────────────────────────────────────────────────────────────
204 have hxcard : ∀ {f : fintype (gpowers x)}, card (gpowers x) = p,
id └─────┘ ┴
src └────────┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─
typ └────────┘ └────┘└─────┘┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴┴└─
doc └────────┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─
txt └────────┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─
par └────────┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─
pid └────────┘ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─
st ─────────────────────────────────────────────────────────────────
205 from λ f, by rw [← hx, order_eq_card_gpowers]; congr,
id └┘ └───────────────────┘
src ──────┘ └──┘ ┴└────┘ └┘└───────────────────┘┴└┘└───┘└┘
typ ──────┘ └──┘ ┴└────┘└┘└┘└───────────────────┘┴└┘└───┘└┘
doc ──────┘ └──┘ ┴└────┘ └┘ ┴└┘ └┘
txt ──────┘ └──┘ ┴└────┘ └┘ ┴└┘└───┘└┘
par ──────┘ └──┘ ┴└────┘ └┘ ┴└┘└───┘└┘
pid ──────┘ └──┘ └─────┘ └┘ └────────┘
st ─────────────┘└───────┘└─────────────────────┘┴└─────┘└─
206 have is_subgroup (mk ⁻¹' gpowers x),
src └───────────┘ ┴ ┴ ┴ └──
typ └───────────┘ ┴ ┴ ┴ └──
doc └───────────┘ ┴ ┴ ┴ └──
txt └───────────┘ ┴ ┴ ┴ └──
par └───────────┘ ┴ ┴ ┴ └──
pid └───────────┘ ┴ ┴ ┴ └──
st ─────────────────────────────────────
207 from is_group_hom.preimage _ _,
id └───────────────────┘
src ──────┘└───────────────────┘└────┘
typ ──────┘└───────────────────┘└────┘
doc ──────┘ └────┘
txt ──────┘ └────┘
par ──────┘ └────┘
pid ──────┘ └────┘
st ──────────────────────────────────
208 have fintype (mk ⁻¹' gpowers x), by apply_instance,
src └───────┘ ┴ ┴ ┴ └────┘└────────────┘└┘
typ └───────┘ ┴ ┴ ┴ └────┘└────────────┘└┘
doc └───────┘ ┴ ┴ ┴ └────┘└────────────┘└┘
txt └───────┘ ┴ ┴ ┴ └────┘└────────────┘└┘
par └───────┘ ┴ ┴ ┴ └────┘└────────────┘└┘
pid └───────┘ ┴ ┴ ┴ └────────────────────┘
st ──────────────────────────────────┘└─────────────┘└─
209 have hequiv : H ≃ (subtype.val ⁻¹' H : set (normalizer H)) :=
id ┴ └─┘ └────────┘
src └────────┘ ┴┴┴ ┴ ┴ └─┘└─┘┴ └────────┘┴ └─────
typ └────────┘ ┴┴┴ ┴ ┴ └─┘└─┘┴ └────────┘┴ └─────
doc └────────┘ ┴┴┴ ┴ ┴ └─┘ ┴ ┴ └─────
txt └────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────
par └────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────
pid └────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────
st ──────────────────────────────────────────────────────────────
210 ⟨λ a, ⟨⟨a.1, subset_normalizer _ a.2⟩, a.2⟩, λ a, ⟨a.1.1, a.2⟩,
id └───────────────┘
src ─┘ └──┘ └──┘└───────────────┘└─┘ └───┘ └───┘ └──┘ └────┘ └────
typ ─┘ └──┘ └──┘└───────────────┘└─┘ └───┘ └───┘ └──┘ └────┘ └────
doc ─┘ └──┘ └──┘ └─┘ └───┘ └───┘ └──┘ └────┘ └────
txt ─┘ └──┘ └──┘ └─┘ └───┘ └───┘ └──┘ └────┘ └────
par ─┘ └──┘ └──┘ └─┘ └───┘ └───┘ └──┘ └────┘ └────
pid ─┘ └──┘ └──┘ └─┘ └───┘ └───┘ └──┘ └────┘ └────
st ──────────────────────────────────────────────────────────────────
211 λ ⟨_, _⟩, rfl, λ ⟨⟨_, _⟩, _⟩, rfl⟩,
id └─┘
src ───┘ └───────┘ └┘ └┘ └─────────┘└─┘└─┘
typ ───┘ └───────┘ └┘ └┘ └─────────┘└─┘└─┘
doc ───┘ └───────┘ └┘ └┘ └─────────┘ └─┘
txt ───┘ └───────┘ └┘ └┘ └─────────┘ └─┘
par ───┘ └───────┘ └┘ └┘ └─────────┘ └─┘
pid ───┘ └───────┘ └┘ └┘ └─────────┘ └─┘
st ────────────────────────────────────────
212 ⟨subtype.val '' (mk ⁻¹' gpowers x), by apply_instance,
id └─────────┘ └┘ └┘ └─────┘
src └─────────┘┴└┘┴ └┘┴ ┴└─────┘┴ └─┘ ┴└────────────┘└─
typ └─────────┘┴└┘┴ └┘┴ ┴└─────┘┴ └─┘ ┴└────────────┘└─
doc ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────────────┘└─
txt ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────────────┘└─
par ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────────────┘└─
pid ┴ ┴ ┴ ┴ ┴ └─┘ └────────────────
st ─────────────────────────────────────┘└─────────────┘└─
213 by rw [set.card_image_of_injective (mk ⁻¹' gpowers x) subtype.val_injective,
id └─────────────────────────┘ └┘ └─────┘ ┴ └───────────────────┘
src ─┘ ┴└──┘└─────────────────────────┘┴ └┘┴ ┴└─────┘┴ └┘└───────────────────┘└─
typ ─┘ ┴└──┘└─────────────────────────┘┴ └┘┴ ┴└─────┘┴┴└┘└───────────────────┘└─
doc ─┘ ┴└──┘ ┴ ┴ ┴ ┴ └┘ └─
txt ─┘ ┴└──┘ ┴ ┴ ┴ ┴ └┘ └─
par ─┘ ┴└──┘ ┴ ┴ ┴ ┴ └┘ └─
pid ─┘ └───┘ ┴ ┴ ┴ ┴ └┘ └─
st ───┘└───────────────────────────────────────────────────────────────────────┘└─
214 nat.pow_succ, ← hH2, fintype.card_congr hequiv, ← hx, order_eq_card_gpowers,
id └──────────┘ └─┘ └────────────────┘ └────┘ └┘ └───────────────────┘
src ─────┘└──────────┘└──┘ └┘└────────────────┘┴ └──┘ └┘└───────────────────┘└─
typ ─────┘└──────────┘└──┘└─┘└┘└────────────────┘┴└────┘└──┘└┘└┘└───────────────────┘└─
doc ─────┘ └──┘ └┘ ┴ └──┘ └┘ └─
txt ─────┘ └──┘ └┘ ┴ └──┘ └┘ └─
par ─────┘ └──┘ └┘ ┴ └──┘ └┘ └─
pid ─────┘ └──┘ └┘ ┴ └──┘ └┘ └─
st ─────────────────┘└─────┘└─────────────────────────┘└────┘└─────────────────────┘└─
215 ← fintype.card_prod];
id └───────────────┘
src ───────┘└───────────────┘┴└─
typ ───────┘└───────────────┘┴└─
doc ───────┘ ┴└─
txt ───────┘ ┴└─
par ───────┘ ┴└─
pid ───────┘ └──
st ────────────────────────┘┴└─
216 exact @fintype.card_congr _ _ (id _) (id _) (preimage_mk_equiv_subgroup_times_set _ _)⟩
id └────────────────┘ └┘ └──────────────────────────────────┘
src ───┘└────┘ └────────────────┘└───┘ └──┘ └┘└──┘ └──────────────────────────────────┘└───┘└─
typ ─────────┘ └────────────────┘└───┘ └──┘ └┘└──┘ └──────────────────────────────────┘└──────
doc ───┘└────┘ └───┘ └──┘ └──┘ └───┘└─
txt ───┘└────┘ └───┘ └──┘ └──┘ └───┘└─
par ─────────┘ └───┘ └──┘ └──┘ └──────
pid ─────────┘ └───┘ └──┘ └──┘ └────┘└
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
217
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
218 end sylow